g:IGroup, a, b:|g|. ~(a * (~(b))) = (b * (~(a)))  |g| 

latex

Up	groups 1
Definitions of Statement	IMonoid, IGroup
Definitions	P  Q, P & Q, t  T, P  Q, P  Q, x f y, x:A. B(x), IMonoid, IGroup
Lemmas	igrp wf, grp inv inv, grp op wf, grp inv wf, grp inv thru op, grp car wf